\begin{tabbing}
R{-}sub\=\{i:l\}\+
\\[0ex]($A$; $B$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=i\=f Rnone?($A$)$\rightarrow$ True\+\+
\\[0ex]; Rplus?($A$)$\rightarrow$ R{-}sub\{i:l\}(Rplus{-}left($A$); $B$) \& R{-}sub\{i:l\}(Rplus{-}right($A$); $B$)
\\[0ex]; Rplus?($B$)$\rightarrow$ R{-}sub\{i:l\}($A$; Rplus{-}left($B$)) $\vee$ R{-}sub\{i:l\}($A$; Rplus{-}right($B$))
\-\\[0ex]else $A$ $=$ $B$ $\in$ es\_realizer\{i:l\} fi
\-\\[0ex]\emph{(recursive)}
\end{tabbing}